Nuprl Lemma : bij_iff_1_1_corr
12,41
postcript
pdf
A
,
B
:Type. (
f
:
A
B
. Bij(
A
;
B
;
f
))
1-1-Corresp(
A
;
B
)
latex
ProofTree
Definitions
,
t
T
,
P
Q
,
P
Q
,
P
&
Q
,
1-1-Corresp(
A
;
B
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
inv
funs
wf
,
biject
wf
,
bij
imp
exists
inv
,
fun
with
inv
is
bij
origin
A, B:Type. (
f:A
B. Bij(A;B;f)) 
1-1-Corresp(A;B)
A, B:Type. (f:AB. Bij(A;B;f)) 1-1-Corresp(A;B)
T Q Qx:A. B(x) Qx:A. B(x)